Crate oxidd_rules_bdd

Rules and other basic definitions for binary decision diagrams (BDDs)

BDDs are represented using binary inner nodes with a level number, and two terminal nodes ⊤ and ⊥. The first outgoing edge (node.get_child(0)) is the “then” edge, the second edge is the “else” edge. Along with the “simple” variant of BDDs, this crate also provides an implementation using complemented edges (here, we elide the ⊥ terminal).

Feature flags

• simple (enabled by default) — Enable the simple BDD implementation
• complement-edge (enabled by default) — Enable the complement edge BDD implementation
• multi-threading (enabled by default) — Enable multi-threaded apply implementations
• statistics — Enable statistics generation

Modules

• complement_edge
  Binary decision diagrams with complemented edges
• simple
  Simple binary decision diagrams (i.e. no complemented edges)